Modular Termination and Combinability for Superposition Modulo Counter Arithmetic
Identifieur interne : 002662 ( Main/Exploration ); précédent : 002661; suivant : 002663Modular Termination and Combinability for Superposition Modulo Counter Arithmetic
Auteurs : Christophe Ringeissen [France] ; Valerio Senni [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Modularity is a highly desirable property in the development of satisfiability procedures. In this paper we are interested in using a dedicated superposition calculus to develop satisfiability procedures for (unions of) theories sharing counter arithmetic. In the first place, we are concerned with the termination of this calculus for theories representing data structures and their extensions. To this purpose, we prove a modularity result for termination which allows us to use our superposition calculus as a satisfiability procedure for combinations of data structures. In addition, we present a general combinability result that permits us to use our satisfiability procedures into a non-disjoint combination method à la Nelson-Oppen without loss of completeness. This latter result is useful whenever data structures are combined with theories for which superposition is not applicable, like theories of arithmetic.
Url:
DOI: 10.1007/978-3-642-24364-6_15
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001567
- to stream Istex, to step Curation: 001549
- to stream Istex, to step Checkpoint: 000562
- to stream Hal, to step Corpus: 003344
- to stream Hal, to step Curation: 003344
- to stream Hal, to step Checkpoint: 001B24
- to stream Main, to step Merge: 002704
- to stream Main, to step Curation: 002662
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Modular Termination and Combinability for Superposition Modulo Counter Arithmetic</title><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name></author><author><name sortKey="Senni, Valerio" sort="Senni, Valerio" uniqKey="Senni V" first="Valerio" last="Senni">Valerio Senni</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:5D6B12F0123A1B5DC0672E07C1C0CAD57E8CFE7F</idno><date when="2011" year="2011">2011</date><idno type="doi">10.1007/978-3-642-24364-6_15</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-VXH7C6KS-8/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001567</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001567</idno><idno type="wicri:Area/Istex/Curation">001549</idno><idno type="wicri:Area/Istex/Checkpoint">000562</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000562</idno><idno type="wicri:doubleKey">0302-9743:2011:Ringeissen C:modular:termination:and</idno><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00636589</idno><idno type="url">https://hal.inria.fr/inria-00636589</idno><idno type="wicri:Area/Hal/Corpus">003344</idno><idno type="wicri:Area/Hal/Curation">003344</idno><idno type="wicri:Area/Hal/Checkpoint">001B24</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">001B24</idno><idno type="wicri:Area/Main/Merge">002704</idno><idno type="wicri:Area/Main/Curation">002662</idno><idno type="wicri:Area/Main/Exploration">002662</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Modular Termination and Combinability for Superposition Modulo Counter Arithmetic</title><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>LORIA-INRIA Nancy Grand Est</wicri:regionArea></affiliation></author><author><name sortKey="Senni, Valerio" sort="Senni, Valerio" uniqKey="Senni V" first="Valerio" last="Senni">Valerio Senni</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>LORIA-INRIA Nancy Grand Est</wicri:regionArea></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Modularity is a highly desirable property in the development of satisfiability procedures. In this paper we are interested in using a dedicated superposition calculus to develop satisfiability procedures for (unions of) theories sharing counter arithmetic. In the first place, we are concerned with the termination of this calculus for theories representing data structures and their extensions. To this purpose, we prove a modularity result for termination which allows us to use our superposition calculus as a satisfiability procedure for combinations of data structures. In addition, we present a general combinability result that permits us to use our satisfiability procedures into a non-disjoint combination method à la Nelson-Oppen without loss of completeness. This latter result is useful whenever data structures are combined with theories for which superposition is not applicable, like theories of arithmetic.</div></front></TEI><affiliations><list><country><li>France</li></country></list><tree><country name="France"><noRegion><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name></noRegion><name sortKey="Senni, Valerio" sort="Senni, Valerio" uniqKey="Senni V" first="Valerio" last="Senni">Valerio Senni</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002662 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 002662 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:5D6B12F0123A1B5DC0672E07C1C0CAD57E8CFE7F
|texte= Modular Termination and Combinability for Superposition Modulo Counter Arithmetic
}}
| This area was generated with Dilib version V0.6.33. |  |